Nuprl Lemma : m-sys-null-compatible-left
0,22
postcript
pdf
M
:Dsys. ||
M
latex
Definitions
t
T
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
Id
,
,
ma-frame-compatible(
A
;
B
)
,
M1
||
M2
,
P
&
Q
,
A
||+
B
,
A
||
B
,
,
MsgA
,
Type
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
Dsys
Lemmas
msga
wf
,
Id
wf
,
ma-empty-compatible-left
,
ma-empty-frame-compatible-left
origin
M:Dsys. || M M:Dsys. || M 
Tx:A. B(x)
B(x)
B(x) B(a)